1. Field of the Present Invention
The present invention generally relates to the field of integrated circuit design verification and more particularly to a method and system for managing verification using modular design verification engines and a verification framework that employ a common interface to facilitate the exchange of verification information and design flows.
2. History of Related Art
As the complexity of microprocessors and other sophisticated integrated circuits has increased over the years, the resources devoted to design verification has accounted for an increasingly large percentage of the total resources required to develop and manufacture an integrated circuit. Indeed, the verification of advanced microprocessors with multiprocessing capability is now estimated to consume more time, labor, and other resources than the actual design of the device.
Traditionally, functional verification has been accomplished by generating a large number of test programs or test cases and running these test programs on a simulator that attempts to model the operation of the device. Designers and verification engineers frequently develop these test cases manually with the help of various random and specific test generators. As the number of transistors, functions, registers, and other facilities in the integrated circuit have increased, conventional verification methods have responded by simply increasing the number of tests that are simulated. Unfortunately, generating a seemingly infinite number of tests is an inefficient and unreliable method of verifying the functionality of all components in the processor.
In the early days of microprocessor development, inefficiencies in functional verification were tolerated because the size of the test space (measured, for example, by the number of states the microprocessor may assume) was sufficiently small. In addition, early microprocessors typically had fewer functional units than modern microprocessors, and the interactions between the components and functions were well understood and controlled. The increasing number of functional units in microprocessors is significant from a verification perspective because interaction between functional units can no longer be ignored or only loosely verified by conventional verification methodologies.
The diverse applications in which modern integrated circuits are employed makes it impossible to predict and plan for the type of software applications that will run on them and thus the state and interdependence that will be exercised in the field are rather large and generally non-deterministic. Roughly speaking, the test space of a microprocessor is approximately equal to 2n where n represents the number of latches (state storage devices) within the microprocessor. From this approximation, it will be appreciated that the test space of microprocessors increases exponentially as the number of latches is increased.
The conventional approach to functional verification, in which increased complexity in a device is verified by simply increasing the number of tests that are simulated, is rapidly becoming infeasible. In addition, because the input to a simulator in a conventional verification process is simply a large number of deterministic tests or randomly generated tests, the output of the simulation must be painstakingly evaluated to determine whether a particular simulation was successful in testing the intended functionality of the device.
It would be desirable to implement a test verification system that addressed the problems associated with design verification. It would be further desirable if the implemented system employed a set of modular and relatively compact verification engines that could be invoked in a determinable sequence. It would be further desirable if the system included a verification framework capable of communicating with a user application program to enable the user to create customized sequences comprised of the modular engines and to apply the customized sequence to a defined verification problem.
The problems identified above are in large part addressed by a design verification system that incorporates a set of modular verification engines within a framework that manages the control flow between the various engines. The framework receives a verification problem from an application, and attempts to solve it by invoking one or more of the engines in a customizable sequence or set of sequences. Each of the verification engines is designed to achieve a specific verification objective. Each of the engines is coded against or complies with a common application program interface (API) to facilitate exchange of information between the engines. The verification engines may include modification engines, which attempt to simplify a problem by modifying it or decomposing it, and decision engines, which attempt to solve problems that are passed to them. As a verification problem is passed from one engine to the next, the engine may alter the verification problem such that a decision engine at the end of the sequence may receive a verification problem that is simpler to solve than the original problem specified by the system user.
If the decision engine is able to solve a problem, such as by determining a state or sequence of states that produces a specified value on a specified node of the design, the decision engine will pass the determined sequence (commonly referred to as a counter example trace) to its parent engine (i.e., the engine that invoked it). Before a trace is passed from a xe2x80x9cchildxe2x80x9d engine to its parent, the engine is responsible for modifying the trace to xe2x80x9cundoxe2x80x9d whatever effect it may have had on the problem. Imagine, for example, a Boolean optimization engine (BOE) receives a netlist or other form of circuit model from the framework and modifies the model by merging two or more nodes before passing the model to a decision engine. If the BOE subsequently receives a trace from the decision engine, the BOE must modify the trace to reflect the existence of all nodes that existed prior to modification by the BOE. In this manner, the framework ultimately receives a netlist that is relevant to the circuit model it started with while the subordinate engines are able to operate on simplified models.